abi: adopt the shared queue ABI (abi_version=1) — re-base QueueError, canonical queue name#78
Merged
Merged
Conversation
… canonical queue name Adopts HAR's shared queue ABI as the single source instead of maintaining an independently-authored copy. Normative source: HAR abi/SHARED-QUEUE-ABI.adoc + Rust binding har-abi. - ProvenQueue.idr: re-base QueueError to the canonical proven-queueconn C-ABI layout — 0=NoError (the NONE success sentinel) + 1..7 for the seven errors. The previous 0..6 numbering diverged from the canonical C header (it claimed to "match proven-queueconn exactly" but did not). Module header now records that this is a *binding of the shared spec*, not an independent declaration. - LinearDispatch.eph: retire the ad-hoc `rpa-events` queue name for the canonical `har.rpa-elysium.inbound` inbound subject, and document RoutedEvent as the consumer-side view of the shared `RoutedEnvelope` (field correspondence noted). Type-level adoption only. A full RoutedEnvelope field-level alignment and a real decoding queue-consumer crate are follow-ups (they need the wire consumer + an Ephapax/Idris build; rpa-elysium's ABI modules are not yet wired to compile, a pre-existing structural item). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 7, 2026
…#79) ## What The ABI (`src/abi/`, Idris2) and FFI (`ffi/zig/`) layers **had never actually built** — no ipkg, module names that didn't resolve, broken proofs, missing FFI glue types, and a Zig `build.zig` on a pre-0.15 API. This wires **both green** and adds `just` recipes to keep them that way. ### Idris2 ABI — `idris2 --build rpa-elysium-abi.ipkg` ✅ (5/5 modules) - New **`rpa-elysium-abi.ipkg`** (sourcedir=`src/abi`; mirrors HAR's `har-abi.ipkg`). - **Flatten** module names to the `src/abi/` layout — this also fixes `Foreign.idr`'s `ABI`-vs-`Abi` **case mismatch** (it imported modules that didn't exist). - **Proof fixes** in `Types.idr`/`Layout.idr`: `eventKindTagValid` / `eventKindTagFitsInByte` every clause wrongly used `LTE 5 5`; each now matches its actual tag (`0→LTEZero`, `1→LTESucc LTEZero`, …). - `Layout.idr`: `import Data.Nat` (`LTE`/`GT` were undefined). - `Foreign.idr`: **define the FFI glue that was referenced but never declared** — `Handle` (+ `createHandle`/`handlePtr`) and `Result` (`Ok=0..NullPointer=4`, matching the Zig enum); fix `registerCallback` to take a raw C-callable pointer (an Idris closure can't be `cast` to `AnyPtr`). ### Zig FFI — `zig build` + `zig build test` ✅ - Port `build.zig` to the **Zig 0.15 API** (`addSharedLibrary`/`addStaticLibrary` → `addLibrary` + shared module + `linkage`; `link_libc` for the C allocator). - Fix `main.zig` for 0.15 (`opaque`-with-fields → `struct`; `callconv(.C)` → `callconv(.c)`). - Produces `librpa_ffi.{a,so}`; tests pass. The **11 exported C symbols match** `Foreign.idr`'s `%foreign` declarations, and the `Result` codes agree. ### Justfile `verify-abi`, `build-ffi`, `test-ffi`, `verify-abi-ffi`. ## Known follow-ups (not compile issues) - `Foreign.idr`'s `process` wrapper treats result `0` as **error** while `processArray` and the Zig side treat `0` as **ok** — the success convention needs reconciling (correctness, with a test). - `generated/abi/` C headers still unimplemented (the formal Idris↔Zig bridge). - `LinearDispatch.eph` (Ephapax) needs its own toolchain to build. Follows the shared-ABI adoption (#78). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Adopts HAR's shared queue ABI as the single source, instead of maintaining
an independently-authored copy of the proven-queueconn types. Normative source:
HAR
abi/SHARED-QUEUE-ABI.adoc+ Rust bindinghar-abi(abi_version = 1).ProvenQueue.idr— re-baseQueueErrorto the canonicalproven-queueconn C-ABI layout:
0 = NoError(theNONEsuccess sentinel)1..7for the seven errors. The previous0..6numbering diverged fromthe canonical C header — the module even claimed to "match proven-queueconn
exactly" but did not. Module header now records that this is a binding of the
shared spec.
LinearDispatch.eph— retire the ad-hocrpa-eventsqueue name for thecanonical
har.rpa-elysium.inboundsubject; documentRoutedEventas theconsumer-side view of the shared
RoutedEnvelope(field correspondencenoted:
eventId↔event_id,kind↔category,payload↔payload, etc.).Mirrors HAR's own
QueueErrorcorrection (hybrid-automation-router #95) so bothsides now agree byte-for-byte.
Scope / follow-ups
Type-level adoption only. Deliberately not in this PR:
RoutedEnvelopefield-level rewrite of the linearRoutedEventtype(would need an Ephapax/Idris checker + the real wire consumer to verify);
rpa-eventstoday isan in-process
tokio::broadcastbus, not a broker client) — greenfield;paths vs file layout — a pre-existing structural item, like HAR's ABI before
it was packaged).
These edits are correct-by-construction, mirroring the verified HAR change.
🤖 Generated with Claude Code